$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $P$:($x$:$A$$\rightarrow$$B$($x$)$\rightarrow\mathbb{P}$), $x$:$A$, $v$:$B$($x$).
\\[0ex]$\forall$$y$$\in$dom($x$ : $v$). $w$=$x$ : $v$($y$) $\Rightarrow$  $P$($y$,$w$) $\Leftarrow\!\Rightarrow$ $P$($x$,$v$)